The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

append(@l1, @l2) → append#1(@l1, @l2)
append#1(::(@x, @xs), @l2) → ::(@x, append(@xs, @l2))
append#1(nil, @l2) → @l2
appendAll(@l) → appendAll#1(@l)
appendAll#1(::(@l1, @ls)) → append(@l1, appendAll(@ls))
appendAll#1(nil) → nil
appendAll2(@l) → appendAll2#1(@l)
appendAll2#1(::(@l1, @ls)) → append(appendAll(@l1), appendAll2(@ls))
appendAll2#1(nil) → nil
appendAll3(@l) → appendAll3#1(@l)
appendAll3#1(::(@l1, @ls)) → append(appendAll2(@l1), appendAll3(@ls))
appendAll3#1(nil) → nil

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

append(@l1, @l2) → append#1(@l1, @l2) [1]
append#1(::(@x, @xs), @l2) → ::(@x, append(@xs, @l2)) [1]
append#1(nil, @l2) → @l2 [1]
appendAll(@l) → appendAll#1(@l) [1]
appendAll#1(::(@l1, @ls)) → append(@l1, appendAll(@ls)) [1]
appendAll#1(nil) → nil [1]
appendAll2(@l) → appendAll2#1(@l) [1]
appendAll2#1(::(@l1, @ls)) → append(appendAll(@l1), appendAll2(@ls)) [1]
appendAll2#1(nil) → nil [1]
appendAll3(@l) → appendAll3#1(@l) [1]
appendAll3#1(::(@l1, @ls)) → append(appendAll2(@l1), appendAll3(@ls)) [1]
appendAll3#1(nil) → nil [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

append(@l1, @l2) → append#1(@l1, @l2) [1]
append#1(::(@x, @xs), @l2) → ::(@x, append(@xs, @l2)) [1]
append#1(nil, @l2) → @l2 [1]
appendAll(@l) → appendAll#1(@l) [1]
appendAll#1(::(@l1, @ls)) → append(@l1, appendAll(@ls)) [1]
appendAll#1(nil) → nil [1]
appendAll2(@l) → appendAll2#1(@l) [1]
appendAll2#1(::(@l1, @ls)) → append(appendAll(@l1), appendAll2(@ls)) [1]
appendAll2#1(nil) → nil [1]
appendAll3(@l) → appendAll3#1(@l) [1]
appendAll3#1(::(@l1, @ls)) → append(appendAll2(@l1), appendAll3(@ls)) [1]
appendAll3#1(nil) → nil [1]

The TRS has the following type information:

append :: :::nil → :::nil → :::nil append#1 :: :::nil → :::nil → :::nil :: :: :::nil → :::nil → :::nil nil :: :::nil appendAll :: :::nil → :::nil appendAll#1 :: :::nil → :::nil appendAll2 :: :::nil → :::nil appendAll2#1 :: :::nil → :::nil appendAll3 :: :::nil → :::nil appendAll3#1 :: :::nil → :::nil

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:
none

And the following fresh constants: none

(6) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: append(@l1, @l2) → append#1(@l1, @l2) [1] append#1(::(@x, @xs), @l2) → ::(@x, append(@xs, @l2)) [1] append#1(nil, @l2) → @l2 [1] appendAll(@l) → appendAll#1(@l) [1] appendAll#1(::(@l1, @ls)) → append(@l1, appendAll(@ls)) [1] appendAll#1(nil) → nil [1] appendAll2(@l) → appendAll2#1(@l) [1] appendAll2#1(::(@l1, @ls)) → append(appendAll(@l1), appendAll2(@ls)) [1] appendAll2#1(nil) → nil [1] appendAll3(@l) → appendAll3#1(@l) [1] appendAll3#1(::(@l1, @ls)) → append(appendAll2(@l1), appendAll3(@ls)) [1] appendAll3#1(nil) → nil [1] The TRS has the following type information: append :: :::nil → :::nil → :::nil append#1 :: :::nil → :::nil → :::nil :: :: :::nil → :::nil → :::nil nil :: :::nil appendAll :: :::nil → :::nil appendAll#1 :: :::nil → :::nil appendAll2 :: :::nil → :::nil appendAll2#1 :: :::nil → :::nil appendAll3 :: :::nil → :::nil appendAll3#1 :: :::nil → :::nil Rewrite Strategy: INNERMOST

(7) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

nil => 0

(8) Obligation:

Complexity RNTS consisting of the following rules:

append(z, z') -{ 1 }→ append#1(@l1, @l2) :|: @l1 >= 0, z' = @l2, @l2 >= 0, z = @l1
append#1(z, z') -{ 1 }→ @l2 :|: z' = @l2, @l2 >= 0, z = 0
append#1(z, z') -{ 1 }→ 1 + @x + append(@xs, @l2) :|: z' = @l2, @x >= 0, z = 1 + @x + @xs, @l2 >= 0, @xs >= 0
appendAll(z) -{ 1 }→ appendAll#1(@l) :|: z = @l, @l >= 0
appendAll#1(z) -{ 1 }→ append(@l1, appendAll(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll#1(z) -{ 1 }→ 0 :|: z = 0
appendAll2(z) -{ 1 }→ appendAll2#1(@l) :|: z = @l, @l >= 0
appendAll2#1(z) -{ 1 }→ append(appendAll(@l1), appendAll2(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll2#1(z) -{ 1 }→ 0 :|: z = 0
appendAll3(z) -{ 1 }→ appendAll3#1(@l) :|: z = @l, @l >= 0
appendAll3#1(z) -{ 1 }→ append(appendAll2(@l1), appendAll3(@ls)) :|: @ls >= 0, @l1 >= 0, z = 1 + @l1 + @ls
appendAll3#1(z) -{ 1 }→ 0 :|: z = 0

Only complete derivations are relevant for the runtime complexity.

(9) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V1),0,[append(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[fun(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[appendAll(V, Out)],[V >= 0]). eq(start(V, V1),0,[fun1(V, Out)],[V >= 0]). eq(start(V, V1),0,[appendAll2(V, Out)],[V >= 0]). eq(start(V, V1),0,[fun2(V, Out)],[V >= 0]). eq(start(V, V1),0,[appendAll3(V, Out)],[V >= 0]). eq(start(V, V1),0,[fun3(V, Out)],[V >= 0]). eq(append(V, V1, Out),1,[fun(V2, V3, Ret)],[Out = Ret,V2 >= 0,V1 = V3,V3 >= 0,V = V2]). eq(fun(V, V1, Out),1,[append(V5, V6, Ret1)],[Out = 1 + Ret1 + V4,V1 = V6,V4 >= 0,V = 1 + V4 + V5,V6 >= 0,V5 >= 0]). eq(fun(V, V1, Out),1,[],[Out = V7,V1 = V7,V7 >= 0,V = 0]). eq(appendAll(V, Out),1,[fun1(V8, Ret2)],[Out = Ret2,V = V8,V8 >= 0]). eq(fun1(V, Out),1,[appendAll(V10, Ret11),append(V9, Ret11, Ret3)],[Out = Ret3,V10 >= 0,V9 >= 0,V = 1 + V10 + V9]). eq(fun1(V, Out),1,[],[Out = 0,V = 0]). eq(appendAll2(V, Out),1,[fun2(V11, Ret4)],[Out = Ret4,V = V11,V11 >= 0]). eq(fun2(V, Out),1,[appendAll(V12, Ret0),appendAll2(V13, Ret12),append(Ret0, Ret12, Ret5)],[Out = Ret5,V13 >= 0,V12 >= 0,V = 1 + V12 + V13]). eq(fun2(V, Out),1,[],[Out = 0,V = 0]). eq(appendAll3(V, Out),1,[fun3(V14, Ret6)],[Out = Ret6,V = V14,V14 >= 0]). eq(fun3(V, Out),1,[appendAll2(V15, Ret01),appendAll3(V16, Ret13),append(Ret01, Ret13, Ret7)],[Out = Ret7,V16 >= 0,V15 >= 0,V = 1 + V15 + V16]). eq(fun3(V, Out),1,[],[Out = 0,V = 0]). input_output_vars(append(V,V1,Out),[V,V1],[Out]). input_output_vars(fun(V,V1,Out),[V,V1],[Out]). input_output_vars(appendAll(V,Out),[V],[Out]). input_output_vars(fun1(V,Out),[V],[Out]). input_output_vars(appendAll2(V,Out),[V],[Out]). input_output_vars(fun2(V,Out),[V],[Out]). input_output_vars(appendAll3(V,Out),[V],[Out]). input_output_vars(fun3(V,Out),[V],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. recursive : [append/3,fun/3]
1. recursive [non_tail] : [appendAll/2,fun1/2]
2. recursive [non_tail] : [appendAll2/2,fun2/2]
3. recursive [non_tail] : [appendAll3/2,fun3/2]
4. non_recursive : [start/2]

#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into append/3
1. SCC is partially evaluated into appendAll/2
2. SCC is partially evaluated into appendAll2/2
3. SCC is partially evaluated into fun3/2
4. SCC is partially evaluated into start/2

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations append/3
* CE 18 is refined into CE [19]
* CE 17 is refined into CE [20]


### Cost equations --> "Loop" of append/3
* CEs [20] --> Loop 10
* CEs [19] --> Loop 11

### Ranking functions of CR append(V,V1,Out)
* RF of phase [11]: [V]

#### Partial ranking functions of CR append(V,V1,Out)
* Partial RF of phase [11]:
- RF of loop [11:1]:
V


### Specialization of cost equations appendAll/2
* CE 14 is refined into CE [21,22]
* CE 13 is refined into CE [23]


### Cost equations --> "Loop" of appendAll/2
* CEs [23] --> Loop 12
* CEs [22] --> Loop 13
* CEs [21] --> Loop 14

### Ranking functions of CR appendAll(V,Out)
* RF of phase [13,14]: [V]

#### Partial ranking functions of CR appendAll(V,Out)
* Partial RF of phase [13,14]:
- RF of loop [13:1]:
V-1
- RF of loop [14:1]:
V


### Specialization of cost equations appendAll2/2
* CE 16 is refined into CE [24,25,26]
* CE 15 is refined into CE [27]


### Cost equations --> "Loop" of appendAll2/2
* CEs [27] --> Loop 15
* CEs [26] --> Loop 16
* CEs [25] --> Loop 17
* CEs [24] --> Loop 18

### Ranking functions of CR appendAll2(V,Out)
* RF of phase [16,17,18]: [V]

#### Partial ranking functions of CR appendAll2(V,Out)
* Partial RF of phase [16,17,18]:
- RF of loop [16:1]:
V-2
- RF of loop [17:1]:
V-1
- RF of loop [18:1]:
V


### Specialization of cost equations fun3/2
* CE 12 is refined into CE [28]
* CE 11 is refined into CE [29,30,31]


### Cost equations --> "Loop" of fun3/2
* CEs [31] --> Loop 19
* CEs [30] --> Loop 20
* CEs [29] --> Loop 21
* CEs [28] --> Loop 22

### Ranking functions of CR fun3(V,Out)
* RF of phase [19,20,21]: [V]

#### Partial ranking functions of CR fun3(V,Out)
* Partial RF of phase [19,20,21]:
- RF of loop [19:1]:
V-2
- RF of loop [20:1]:
V-1
- RF of loop [21:1]:
V


### Specialization of cost equations start/2
* CE 2 is refined into CE [32,33]
* CE 3 is refined into CE [34]
* CE 4 is refined into CE [35,36,37,38,39,40]
* CE 5 is refined into CE [41,42,43,44]
* CE 6 is refined into CE [45,46]
* CE 7 is refined into CE [47,48]
* CE 8 is refined into CE [49,50]
* CE 9 is refined into CE [51,52]
* CE 10 is refined into CE [53,54]


### Cost equations --> "Loop" of start/2
* CEs [33,35,36,37,38,39,40,41,42,43,44,45,46,48,50,52,54] --> Loop 23
* CEs [32,34,47,49,51,53] --> Loop 24

### Ranking functions of CR start(V,V1)

#### Partial ranking functions of CR start(V,V1)


Computing Bounds
=====================================

#### Cost of chains of append(V,V1,Out):
* Chain [[11],10]: 2*it(11)+2
Such that:it(11) =< -V1+Out

with precondition: [V+V1=Out,V>=1,V1>=0]

* Chain [10]: 2
with precondition: [V=0,V1=Out,V1>=0]


#### Cost of chains of appendAll(V,Out):
* Chain [[13,14],12]: 10*it(13)+2
Such that:aux(3) =< V
it(13) =< aux(3)

with precondition: [Out>=0,V>=Out+1]

* Chain [12]: 2
with precondition: [V=0,Out=0]


#### Cost of chains of appendAll2(V,Out):
* Chain [[16,17,18],15]: 40*it(16)+2
Such that:aux(7) =< V
it(16) =< aux(7)

with precondition: [Out>=0,V>=Out+1]

* Chain [15]: 2
with precondition: [V=0,Out=0]


#### Cost of chains of fun3(V,Out):
* Chain [[19,20,21],22]: 100*it(19)+1
Such that:aux(11) =< V
it(19) =< aux(11)

with precondition: [Out>=0,V>=Out+1]

* Chain [22]: 1
with precondition: [V=0,Out=0]


#### Cost of chains of start(V,V1):
* Chain [24]: 2
with precondition: [V=0]

* Chain [23]: 442*s(31)+7
Such that:aux(16) =< V
s(31) =< aux(16)

with precondition: [V>=1]


Closed-form bounds of start(V,V1):
-------------------------------------
* Chain [24] with precondition: [V=0]
- Upper bound: 2
- Complexity: constant
* Chain [23] with precondition: [V>=1]
- Upper bound: 442*V+7
- Complexity: n

### Maximum cost of start(V,V1): 442*V+7
Asymptotic class: n
* Total analysis performed in 301 ms.

(10) BOUNDS(1, n^1)